package edu.uic.cs.cs582.process.impl;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;
import java.util.TreeSet;

import org.apache.log4j.Logger;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;

import edu.uic.cs.cs582.data.Component;
import edu.uic.cs.cs582.data.Synset;
import edu.uic.cs.cs582.data.SynsetSet;
import edu.uic.cs.cs582.data.Word;
import edu.uic.cs.cs582.misc.Config;
import edu.uic.cs.cs582.misc.GeneralException;
import edu.uic.cs.cs582.misc.LogHelper;
import edu.uic.cs.cs582.process.SatProcessor;
import edu.uic.cs.cs582.process.impl.SatIndexParser.Index;
import edu.uic.cs.cs582.process.impl.SatIndexParser.SynsetIndex;

public class SatProcessorImpl implements SatProcessor
{
	private static final Logger LOGGER = LogHelper
			.getLogger(SatProcessorImpl.class);

	private TreeSet<Integer> conflictSynsetIndexes = new TreeSet<Integer>();
	private TreeSet<Integer> conflictWordIndexes = new TreeSet<Integer>();

	private Component component = null;

	public SatProcessorImpl(Component component)
	{
		this.component = component;
	}

	@Override
	public boolean processSat(int[][] cnfArrays) throws TimeoutException
	{
		ISolver solver = SolverFactory.newDefault();
		solver.newVar(Config.MAXVAR);
		solver.setTimeoutMs(Config.TIMEOUT);
		for (int[] clause : cnfArrays)
		{
			try
			{
				//				System.out.println(Arrays.toString(clause));
				solver.addClause(new VecInt(clause));
			}
			catch (ContradictionException e)
			{
				//				System.out.println(e.getMessage());
				if (LOGGER.isDebugEnabled())
				{
					LOGGER.debug("Catch ContradictionException. ");
				}

				//				int iii = ((WordIndex) SatIndexParser.parseIndex(11,
				//						component)).getWordIndexInOneComponent();
				//				System.out.println(component.getWordByIndex(iii));

				for (int i : clause)
				{
					Index index = SatIndexParser.parseIndex(i, component);
					if (index instanceof SynsetIndex)
					{
						conflictSynsetIndexes.add(((SynsetIndex) index)
								.getSynsetIndex());
						//						System.out.println("*************** early synset: "
						//								+ i
						//								+ " "
						//								+ component
						//										.getSynsetByIndex(((SynsetIndex) index)
						//												.getSynsetIndex()));
					}
					//					else if (index instanceof WordIndex)
					//					{
					//						conflictWordIndexes.add(((WordIndex) index)
					//								.getWordIndexInOneComponent());
					//						//						System.out.println("*************** early word: "
					//						//								+ i
					//						//								+ " "
					//						//								+ component
					//						//										.getWordByIndex(((WordIndex) index)
					//						//												.getWordIndexInOneComponent()));
					//					}
				}
			}
		}

		// if there's conflict happening when add variables into the solver,
		// return false, and there's no need for further checking
		if (!conflictSynsetIndexes.isEmpty() || !conflictWordIndexes.isEmpty())
		{
			return false;
		}
		/////////////////////

		solver.setSearchListener(new ConflictDetectingListener(
				conflictSynsetIndexes, conflictWordIndexes, component));

		LOGGER.debug("Begin to solve SAT. ");
		boolean result = solver.isSatisfiable();
		LOGGER.debug("End to solve SAT. Result is [" + result + "]. ");

		return result;
	}

	private Set<Synset> getConflictSynset()
	{
		HashSet<Synset> result = new HashSet<Synset>(
				conflictSynsetIndexes.size());
		for (Integer index : conflictSynsetIndexes)
		{
			result.add(component.getSynsetByIndex(index));
		}

		//		Map<SynsetSet, Set<Word>> conflictingWordsByMajoritySynsets = initializeConflictingSynsetsSet();
		//		for (SynsetSet set : conflictingWordsByMajoritySynsets.keySet())
		//		{
		//			result.addAll(set);
		//		}

		return result;
	}

	/*public Map<Synset, Set<Word>> getConflictWordsBySynset()
	{
		Map<Synset, Set<Word>> result = new HashMap<Synset, Set<Word>>();

		Set<Word> allWords = component.getAllWords();
		Set<Synset> allConflictSynsets = getConflictSynset();

		boolean hasChanged = false;
		do
		{
			hasChanged = false;

			for (Word word : allWords)
			{
				if (isWordContainsNonConflictMajoritySynset(word,
						allConflictSynsets))
				{
					continue;
				}

				if (!hasChanged
						&& allConflictSynsets.addAll(word
								.getAllSynsetsInMajoritySynsets()))
				{
					hasChanged = true;
				}

				for (Synset conflictingSynset : word
						.getAllSynsetsInMajoritySynsets())
				{
					//					if (isOneMajoritySynsetContainsGivenSynset(word,
					//							conflictingSynset))
					//					{
					Set<Word> wordList = result.get(conflictingSynset);
					if (wordList == null)
					{
						wordList = new TreeSet<Word>();
						result.put(conflictingSynset, wordList);
					}
					wordList.add(word);
					//					}
				}

			}
		}
		while (hasChanged);

		// post-process, remove all conflict list contain only one word
		Iterator<Entry<Synset, Set<Word>>> iterator = result.entrySet()
				.iterator();
		while (iterator.hasNext())
		{
			Set<Word> words = iterator.next().getValue();
			if (words.size() == 1)
			{
				iterator.remove();
			}
		}

		return result;
	}*/

	@Override
	public Map<Synset, Set<Word>> getConflictWordsBySynset()
	{
		Map<Synset, Set<Word>> result = new HashMap<Synset, Set<Word>>();

		Set<Word> allWords = component.getAllWords();
		Set<Synset> allConflictSynsets = getConflictSynset();

		//		if (allConflictSynsets.isEmpty())
		//		{
		//			return result;
		//		}

		for (Word word : allWords)
		{
			if (isWordContainsNonConflictMajoritySynset(word,
					allConflictSynsets))
			{
				continue;
			}

			// here, all majority-synsets contain some conflict synset
			// we need to get a map to tell which word has which synsets
			for (Synset conflictingSynset : allConflictSynsets)
			{
				if (doesAnyMajoritySynsetContainGivenSynset(word,
						conflictingSynset))
				{
					Set<Word> wordList = result.get(conflictingSynset);
					if (wordList == null)
					{
						wordList = new TreeSet<Word>();
						result.put(conflictingSynset, wordList);
					}
					wordList.add(word);
				}
			}
		}

		//		Map<Synset, Set<Word>> resultFromConflictWords = getConflictWordsBySynsetsInMajority();
		//		result = combineTwoResult(result, resultFromConflictWords);

		//		Iterator<Entry<Synset, Set<Word>>> iter = result.entrySet().iterator();
		//		while (iter.hasNext())
		//		{
		//			Entry<Synset, Set<Word>> entry = iter.next();
		//			if (entry.getValue().size() == 1)
		//			{
		//				iter.remove();
		//			}
		//		}

		return result;
	}

	//	private Map<Synset, Set<Word>> combineTwoResult(
	//			Map<Synset, Set<Word>> result,
	//			Map<Synset, Set<Word>> resultFromConflictWords)
	//	{
	//		for (Entry<Synset, Set<Word>> entry : resultFromConflictWords
	//				.entrySet())
	//		{
	//			Synset keySynset = entry.getKey();
	//			if (!result.containsKey(keySynset))
	//			{
	//				result.put(keySynset, new HashSet<Word>());
	//			}
	//			result.get(keySynset).addAll(entry.getValue());
	//		}
	//
	//		return result;
	//	}

	private boolean isWordContainsNonConflictMajoritySynset(Word word,
			Set<Synset> allConflictSynsets)
	{
		for (Set<Synset> eachMajority : word.getMajoritySynsets())
		{
			boolean isMajorityContainsConflict = false;
			for (Synset eachConflictSynset : allConflictSynsets)
			{
				if (eachMajority.contains(eachConflictSynset))
				{
					isMajorityContainsConflict = true;
					break;
				}
			}

			if (!isMajorityContainsConflict)
			{
				return true;
			}
		}

		return false;
	}

	public boolean doesAnyMajoritySynsetContainGivenSynset(Word word,
			Synset conflictingSynset)
	{
		for (SynsetSet eachMajoritySynsets : word.getMajoritySynsets())
		{
			if (eachMajoritySynsets.contains(conflictingSynset))
			{
				return true;
			}
		}

		return false;
	}

	@Override
	public Map<SynsetSet, Set<Word>> getConflictWordsBySynsetsInMajority()
	{
		throw new GeneralException(new UnsupportedOperationException());
	}

	/*@Override
	public Map<SynsetSet, Set<Word>> getConflictWordsBySynsetsInMajority()
	{
		Map<SynsetSet, Set<Word>> conflictingWordsBySynsetSetInMajority = initializeConflictingSynsetsSet();
		Set<SynsetSet> allKnownConflictingSynsetSetsInMajority = conflictingWordsBySynsetSetInMajority
				.keySet();

		for (Word word : component.getAllWords())
		{
			Integer otherWordIndex = component.getIndexOfWord(word);
			if (conflictWordIndexes.contains(otherWordIndex))
			{
				// the conflicting words that have already processed in above steps
				continue;
			}

			if (isWordConflictingInAllItsMajoritySynsets(word,
					allKnownConflictingSynsetSetsInMajority))
			{
				for (SynsetSet synsetSet : word.getMajoritySynsets())
				{
					Set<Word> conflictingWords = conflictingWordsBySynsetSetInMajority
							.get(synsetSet);
					if (conflictingWords == null)
					{
						conflictingWords = new TreeSet<Word>();
						conflictingWordsBySynsetSetInMajority.put(synsetSet,
								conflictingWords);
					}
					conflictingWords.add(word);
				}
			}
		}

		return conflictingWordsBySynsetSetInMajority;
	}*/

	//	private boolean isWordConflictingInAllItsMajoritySynsets(Word word,
	//			Set<SynsetSet> allKnownConflictingMajoritySynsets)
	//	{
	//		List<SynsetSet> allMajoritySynsetsOfWord = word.getMajoritySynsets();
	//
	//		// if word has only one majority, 
	//		// and the only one has common with any known conflict SynsetSet of some majority
	//		if (allMajoritySynsetsOfWord.size() == 1)
	//		{
	//			SynsetSet theOnlyOneMajority = allMajoritySynsetsOfWord.get(0);
	//			for (SynsetSet knownConflictingSynsetSet : allKnownConflictingMajoritySynsets)
	//			{
	//				if (knownConflictingSynsetSet.hasCommon(theOnlyOneMajority))
	//				{
	//					return true;
	//				}
	//			}
	//		}
	//		// if word has more than one majorities, 
	//		// make sure all of them are equal to some known conflict SynsetSet of some majority 
	//		else
	//		{
	//			return allKnownConflictingMajoritySynsets
	//					.containsAll(allMajoritySynsetsOfWord);
	//		}
	//
	//		return false;
	//	}

	//	private Set<Synset> getAllConflictSynsets(
	//			Map<SynsetSet, Set<Word>> conflictingWordsByMajoritySynsets)
	//	{
	//		Set<Synset> result = new HashSet<Synset>();
	//		for (SynsetSet set : conflictingWordsByMajoritySynsets.keySet())
	//		{
	//			result.addAll(set);
	//		}
	//
	//		return result;
	//	}

	/*// @Override
	public Map<SynsetSet, Set<Word>> getConflictWordsByMajoritySynsets2()
	{
		Map<SynsetSet, Set<Word>> conflictingWordsByMajoritySynsets = initializeConflictingSynsetsSet();

		//		boolean hasChanged = false;
		//		do
		//		{
		//			hasChanged = false;

		for (Word word : component.getAllWords())
		{
			Integer otherWordIndex = component.getIndexOfWord(word);
			if (conflictWordIndexes.contains(otherWordIndex))
			{
				// the conflicting words that have already processed in above steps
				continue;
			}

			// if one word has only one majority-synset, 
			// and the majority-synset has common with some known as inconsistent
			SynsetSet commonSynsetSet = getTheOnlyOneMajoritySynsetsWhichIsInConflicting(
					word, conflictingWordsByMajoritySynsets);
			if (commonSynsetSet != null)
			{
				conflictWordIndexes.add(otherWordIndex);
				Set<Word> conflictingWords = conflictingWordsByMajoritySynsets
						.get(commonSynsetSet);
				if (conflictingWords == null)
				{
					conflictingWords = new TreeSet<Word>();
					conflictingWordsByMajoritySynsets.put(commonSynsetSet,
							conflictingWords);
					//						hasChanged = true;
				}
				conflictingWords.add(word);

				continue;
			}

			// the words that haven't been reported, but may be the cause of conflict

			// if word doesn't have free majority-synsets
			// the word must be inconsistent
			if (!hasConflictFreeMajoritySynsets(word,
					conflictingWordsByMajoritySynsets))
			{
				conflictWordIndexes.add(otherWordIndex);

				for (SynsetSet majoritySynsetsOfWord : word
						.getMajoritySynsets())
				{
					Set<Word> conflictingWords = conflictingWordsByMajoritySynsets
							.get(majoritySynsetsOfWord);
					if (conflictingWords == null)
					{
						conflictingWords = new TreeSet<Word>();
						conflictingWordsByMajoritySynsets.put(
								majoritySynsetsOfWord, conflictingWords);
						//							hasChanged = true;
					}
					conflictingWords.add(word);
				}
			}
		}
		//		}
		//		while (hasChanged);

		return conflictingWordsByMajoritySynsets;
	}

	private SynsetSet getTheOnlyOneMajoritySynsetsWhichIsInConflicting(
			Word word,
			Map<SynsetSet, Set<Word>> conflictingWordsByMajoritySynsets)
	{
		for (Entry<SynsetSet, Set<Word>> knownConflicting : conflictingWordsByMajoritySynsets
				.entrySet())
		{
			SynsetSet conflictingMajoritySynsets = knownConflicting.getKey();
			List<SynsetSet> allMajoritySynsetsOfTheWord = word
					.getMajoritySynsets();
			if (allMajoritySynsetsOfTheWord.size() == 1
					&& allMajoritySynsetsOfTheWord.get(0).hasCommon(
							conflictingMajoritySynsets))
			{
				return allMajoritySynsetsOfTheWord.get(0);
			}
		}

		return null;
	}*/

	// if a word is said to be inconsistent, all its majority-synsets must be inconsistent, 
	// otherwise the certain polarity can be assigned to that 'conflict-free' majority-synsets 
	//	private Map<SynsetSet, Set<Word>> initializeConflictingSynsetsSet()
	//	{
	//		Map<SynsetSet, Set<Word>> result = new HashMap<SynsetSet, Set<Word>>();
	//
	//		// for each conflicting word
	//		List<Integer> conflictIndexList = new ArrayList<Integer>(
	//				conflictWordIndexes);
	//		if (conflictIndexList.size() == 1)
	//		{
	//			Word conflictingWord = component.getWordByIndex(conflictIndexList
	//					.get(0));
	//			for (SynsetSet set : conflictingWord.getMajoritySynsets())
	//			{
	//				TreeSet<Word> conflictingWords = new TreeSet<Word>();
	//				conflictingWords.add(conflictingWord);
	//				result.put(set, conflictingWords);
	//			}
	//
	//		}
	//		else
	//		{
	//			for (int i = 0; i < conflictIndexList.size(); i++)
	//			{
	//				Word conflictingWord = component
	//						.getWordByIndex(conflictIndexList.get(i));
	//				for (int j = i + 1; j < conflictIndexList.size(); j++)
	//				{
	//					Word anotherConflictWord = component
	//							.getWordByIndex(conflictIndexList.get(j));
	//					Set<SynsetSet> commonSynsetsSet = getCommonSynsetsInMajority(
	//							conflictingWord, anotherConflictWord);
	//
	//					if (commonSynsetsSet == null)
	//					{
	//						continue;
	//					}
	//
	//					for (SynsetSet commonSynsets : commonSynsetsSet)
	//					{
	//						Set<Word> conflictingWords = result.get(commonSynsets);
	//						if (conflictingWords == null)
	//						{
	//							conflictingWords = new TreeSet<Word>();
	//							result.put(commonSynsets, conflictingWords);
	//						}
	//						conflictingWords.add(conflictingWord);
	//						conflictingWords.add(anotherConflictWord);
	//					}
	//				}
	//			}
	//		}
	//
	//		return result;
	//	}
	//
	//	private Set<SynsetSet> getCommonSynsetsInMajority(Word conflictingWord,
	//			Word anotherConflictWord)
	//	{
	//		if (conflictingWord == anotherConflictWord
	//				|| conflictingWord.getPolarity().equals(
	//						anotherConflictWord.getPolarity()))
	//		{
	//			return null;
	//		}
	//
	//		Set<SynsetSet> result = new HashSet<SynsetSet>();
	//
	//		List<SynsetSet> allMajoritySynsetsInOneWord = conflictingWord
	//				.getMajoritySynsets();
	//		List<SynsetSet> allMajoritySynsetsInAnotherWord = anotherConflictWord
	//				.getMajoritySynsets();
	//
	//		for (SynsetSet majorityOne : allMajoritySynsetsInOneWord)
	//		{
	//			for (SynsetSet majorityTwo : allMajoritySynsetsInAnotherWord)
	//			{
	//				SynsetSet commonSynsets = getCommonSynsetsOF(majorityOne,
	//						majorityTwo);
	//				if (commonSynsets != null)
	//				{
	//					result.add(commonSynsets);
	//				}
	//			}
	//		}
	//
	//		return result.isEmpty() ? null : result;
	//	}
	//
	//	private SynsetSet getCommonSynsetsOF(SynsetSet majorityOne,
	//			SynsetSet majorityTwo)
	//	{
	//		SynsetSet common = new SynsetSet();
	//
	//		if (majorityOne.size() > majorityTwo.size())
	//		{
	//			SynsetSet temp = majorityOne;
	//			majorityOne = majorityTwo;
	//			majorityTwo = temp;
	//		}
	//
	//		for (Synset one : majorityOne)
	//		{
	//			if (majorityTwo.contains(one))
	//			{
	//				common.add(one);
	//			}
	//		}
	//
	//		return common.isEmpty() ? null : common;
	//	}

	//	private boolean hasConflictFreeMajoritySynsets(Word word,
	//			Map<SynsetSet, Set<Word>> allKnownConflictingMajoritySynsets)
	//	{
	//		for (SynsetSet majoritySynsetsOfWord : word.getMajoritySynsets())
	//		{
	//			boolean hasCommon = false;
	//			for (SynsetSet knownConflictingMajoritySynsets : allKnownConflictingMajoritySynsets
	//					.keySet())
	//			{
	//				// the polarities should not be the same one
	//				// has no common -> there is free
	//				if (majoritySynsetsOfWord
	//						.hasCommon(knownConflictingMajoritySynsets))
	//				{
	//					hasCommon = true;
	//					break;
	//				}
	//			}
	//
	//			if (!hasCommon)
	//			{
	//				return true;
	//			}
	//		}
	//
	//		return false;
	//	}
}
